(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 6))
(let ((e4 1))
(let ((e5 (- v2 v1)))
(let ((e6 (+ v1 e5)))
(let ((e7 (* v0 (- e4))))
(let ((e8 (- e5)))
(let ((e9 (/ e4 e3)))
(let ((e10 (< e7 e5)))
(let ((e11 (>= e6 v1)))
(let ((e12 (< v2 e8)))
(let ((e13 (>= v0 e9)))
(let ((e14 (= e9 e7)))
(let ((e15 (>= v0 e9)))
(let ((e16 (= v0 e5)))
(let ((e17 (distinct v1 e6)))
(let ((e18 (distinct e8 e7)))
(let ((e19 (>= v0 e8)))
(let ((e20 (<= v2 e8)))
(let ((e21 (and e17 e16)))
(let ((e22 (and e14 e11)))
(let ((e23 (ite e13 e21 e21)))
(let ((e24 (or e15 e12)))
(let ((e25 (= e24 e18)))
(let ((e26 (or e22 e10)))
(let ((e27 (=> e19 e23)))
(let ((e28 (xor e25 e26)))
(let ((e29 (xor e20 e20)))
(let ((e30 (=> e27 e29)))
(let ((e31 (and e30 e30)))
(let ((e32 (not e31)))
(let ((e33 (not e28)))
(let ((e34 (and e32 e33)))
e34
)))))))))))))))))))))))))))))))))

;; CHECK: (assert (= v0 (/ 42 49)))
;; CHECK: (assert (= v1 (/ 8 (- 45))))
;; CHECK: (check-sat)
(check-sat-assuming-model (v0 v1) ((/ 42 49) (/ 8 (- 45))))
